package model.directory;

import model.logic.Conjunction;
import model.logic.Disjunction;
import model.logic.Proposition;
import model.logic.operand.Variable;
import model.logic.operator.OpEqual;
import model.logic.operator.OpLess;
import model.logic.operator.OpMinusEqual;
import model.types.Int;
import model.types.Nat;
import model.types.Rat;

public final class MethodProvider {
	
	/**
	 * Base of decimal-system. 
	 */
	private static final int BASE_DECIMAL = 10;
	/**
	 * Treshold for rounding decimal Rats. 
	 */
	private static final int ROUND_TRESHOLD_DECIMAL = 5;
	/**
	 * Identifier for the result-variable. 
	 */
	private static final String VARIABLE_IDENTIFIER_RESULT = "result";
	/**
	 * Identifier for the varibale x. 
	 */
	private static final String VARIABLE_IDENTIFIER_X = "x";
	
	private MethodProvider() {
		
	}
	
	
	/**
	 * Returns the annotation for operation: abs. 
	 * @return annotation
	 */
	public static Disjunction getAbsAnnotation() {
		Variable x = new Variable(VARIABLE_IDENTIFIER_X);
		Variable result = new Variable(VARIABLE_IDENTIFIER_RESULT);
		Proposition prop1 = new Proposition(true, OpLess.getInstance(), x);
		Proposition prop2 = new Proposition(false, OpEqual.getInstance(), result , x);
		Proposition prop3 = new Proposition(false, OpLess.getInstance(), x);
		Proposition prop4 = new Proposition(false, OpMinusEqual.getInstance(), result, x);
		Conjunction conj1 = new Conjunction();
		conj1.addProposition(prop1);
		conj1.addProposition(prop2);
		Conjunction conj2 = new Conjunction();
		conj2.addProposition(prop3);
		conj2.addProposition(prop4);	
		Disjunction disj = new Disjunction();
		disj.addConjunction(conj1);
		disj.addConjunction(conj2);
		return disj;
	}
	
	/**
	 * Calcs absolute value of x. 
	 * @param x <tt>Int</tt> to build the absolute value of
	 * @return absolute value of <tt>x</tt>
	 */
	public static Nat abs(Int x) {
		int num = x.getNumerator();
		return num < 0 
		       ? new Nat(num * -1) : new Nat(num);
	}
	
	/**
	 * Rounds <tt>x</tt> to the next <tt>Nat</tt>. 
	 * 0,5 -> 1 
	 * @param x Rat to be rounded
	 * @return rounded value of <tt>x</tt>
	 */
	public static Int round(final Rat x) {
		final int quot = x.getNumerator() * BASE_DECIMAL / x.getDenominator();
		int res = quot / BASE_DECIMAL;
		return quot % BASE_DECIMAL < ROUND_TRESHOLD_DECIMAL ? new Int(res) : new Int(++res);
	}
	
	
	/**
	 * Rounds x with n post-comma decimals.  
	 * @param x Rat to be rounded  
	 * @param n count of post-comma decimals 
	 * @return rounded <tt>x</tt>
	 */
	public static Rat round(final Rat x, final Nat n) {
		final int shift = MethodProvider.power(new Nat(BASE_DECIMAL), new Int(n.getNumerator())).getNumerator();
		final int quot = x.getNumerator() * shift * BASE_DECIMAL / x.getDenominator();
		int res = quot / BASE_DECIMAL;
		return quot % BASE_DECIMAL < ROUND_TRESHOLD_DECIMAL ? new Rat(res, shift) : new Rat(++res, shift);
	}
	
	
	/**
	 * Builds a^b. 
	 * @param a base
	 * @param b exponent
	 * @return a^b
	 */
	public static Rat power(final Nat a, final Int b) {
		if (b.getNumerator() >= 0) {
			int result = 1;
			for (int i = 0; i < b.getNumerator(); i++) {
				result *= a.getNumerator();
			}
			return new Nat(result);
		} else {
			return new Rat(1, MethodProvider.power(a, MethodProvider.abs(b)).getNumerator());
		}
	}
}
